Aloul, “Using SAT-based techniques

Power consumption of synchronous sequential circuits can be reduced by careful encoding of the states of the circuit. The idea is to reduce the average number of bit changes per state transition by ¯nding an optimal state assignment. This state assignment problem is NP-hard, and existing techniques rely mainly on heuristic-based methods. The primary goal of this work is to assess the suitability of using complete advanced Boolean Satis¯ability and Integer Linear Programming (ILP) methods in ¯nding an optimized solution. We formulate the problem as a 0-1 ILP instance with power minimization being the objective. Using generic and commercial solvers, the pro-posed approach was tested on sample circuits from the MCNC benchmark suite. Furthermore, in an e®ort to accelerate the search process, circuits were checked for symmetries and symmetry breaking predicates were added whenever applicable. The experimental results provide a pragmatic insight into the problem and basis for further exploration